# This file is part of Acacia+, a tool for synthesis of reactive systems using antichain-based techniques
# Copyright (C) 2011-2013 UMONS-ULB
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
# 
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
# 
# You should have received a copy of the GNU General Public License along
# with this program; if not, write to the Free Software Foundation, Inc.,
# 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.

from pygraph.classes.digraph import *
import subprocess
import os

from constants import *
from utils import *
    
#### Writes an automaton into gff format (to give to Quasy)
def write_automaton_for_quasy(inputs, outputs, initial_states, states, starting_player, label_values, path, filename):
    # Headers      
    gff_content = '<?xml version="1.0" encoding="UTF-8" standalone="no"?>\n'
    gff_content += '<structure label-on="transition" type="fa">\n'
    # Alphabet
    gff_content += '<alphabet type="propositional">\n'
    prop_map = dict() # mapping from propositions from inputs+outputs to propositions id in gff format
    for i in range(len(inputs)):
        gff_content += '<prop>r'+str(i)+'</prop>\n'
        prop_map[inputs[i]] = 'r'+str(i) 
    for i in range(len(outputs)):
        gff_content += '<prop>g'+str(i)+'</prop>\n'
        prop_map[outputs[i]] = 'g'+str(i) 
    gff_content += '</alphabet>\n'
    # States
    gff_content += '<stateSet>\n'
    states_map = dict() # mapping from states id in states list to states id in gff format
    state_id=0
    for s in states:
        (player, transitions) = states[s]
        if player == starting_player:
            gff_content += '<state sid="'+str(state_id)+'"></state>\n'
            states_map[s] = state_id
            state_id+=1
    gff_content += '</stateSet>\n'
    # Transitions
    gff_content += '<transitionSet>\n'
    prop_map_inv = invert_dict(prop_map) # mapping from propositions id in gff format to propositions from inputs+outputs
    tr_id=0
    for s in states:
        (s_player, s_transitions) = states[s]
        if s_player == starting_player:
            cur_s_id = str(states_map[s])
            for s_label in s_transitions:
                cur_s_label = convert_label_to_gff_format(s_label, prop_map)
                cur_s_label_val = label_values[s_label]
                for s_to in s_transitions[s_label]:
                    (o_player, o_transitions) = states[s_to]
                    for o_label in o_transitions:
                        cur_label = cur_s_label + " " + convert_label_to_gff_format(o_label, prop_map)
                        cur_label_val = str(cur_s_label_val + label_values[o_label])
                        for o_to in o_transitions[o_label]:
                            gff_content += '<transition tid="'+str(tr_id)+'">\n'
                            gff_content += '<from>'+cur_s_id+'</from>\n'
                            gff_content += '<to>'+str(states_map[o_to])+'</to>\n'
                            
                            gff_content += '<read>'+cur_label+' w'+cur_label_val+'</read>\n'
                            gff_content += '</transition>\n'                    
                            tr_id+=1
    gff_content += '</transitionSet>\n'
    # Initial states
    gff_content += '<initialStateSet>\n'
    for s in initial_states:
        gff_content += '<stateID>'+str(states_map[s])+'</stateID>\n'
    gff_content += '</initialStateSet>\n'
    gff_content += '</structure>\n'
  
    gff_file_string = path + filename + ".gff"
    gff_file = open(gff_file_string, "w")                  
    gff_file.write(gff_content)
    gff_file.close()
    
    return (gff_file_string, prop_map_inv)

#### Converts a label of transition to gff format (! -> ~, && -> , system signals -> gi, environment signals -> ri)
def convert_label_to_gff_format(label, prop_map):
    label = label.replace(" && ", " ")
    label = label.replace("!", "~")
    for prop in prop_map:
        label = label.replace(prop, prop_map[prop].swapcase())
    return label.swapcase()

#### Converts a label of transition from gff format (~ -> !, -> && , gi -> system signals, ri -> environment signals)
def convert_label_from_gff_format(label, prop_map, inputs, outputs, starting_player):
    #label = label.lstrip().rstrip().replace(" ", " && ")
    label = label.replace("~", "!")
    for prop in prop_map:
        label = label.replace(prop, prop_map[prop].swapcase())
    label = label.swapcase()
    label_i = ""
    for i in inputs:
        if '!'+i in label:
            label_i += '!'+i+" "
        else:
            label_i += i+" "
    label_o = ""
    for o in outputs:
        if '!'+o in label:
            label_o += '!'+o+" "
        else:
            label_o += o+" "
    return "((" + label_o.lstrip().rstrip().replace(" ", " && ") + ") U (" + label_i.lstrip().rstrip().replace(" ", " && ") +"))"

#### Calls Quasy to compute best average case strategy from automaton in gff_file
def call_quasy(gff_file, path, filename, verbosity):
    start_time = start_time = os.times()[4]
    
    controled_print("Calling Quasy to select best average case strategy among computed strategies\n", [MINTEXT, ALLTEXT], verbosity)
    out = subprocess.Popen(['scala', '-classpath', QUASY_PATH+"bin", "quasy.Main", 'solveMDP', gff_file, QUASY_PATH+'run_files/safety_automaton.gff', QUASY_PATH+'run_files/uniform_dist.txt', path + '/'+filename+'_Quasy/'],stdout=subprocess.PIPE)
    (result, error) = out.communicate()
    
    quasy_result_file = open(path + '/'+filename+"_Quasy/results.quasy", "w")              
    quasy_result_file.write(result)
    quasy_result_file.close()
    
    controled_print("Results of Quasy written at " + path +filename+"_Quasy/\n", [ALLTEXT, MINTEXT], verbosity)
    
    controled_print(result+"\n", [ALLTEXT], verbosity)
    quasy_time = os.times()[4]-start_time
    controled_print("Quasy time: %.2fs\n" % quasy_time, [MINTEXT, ALLTEXT], verbosity)
    
    return path + '/'+filename+"_Quasy/MealyMachine.gff"


#### Converts the mealy machine output by Quasy in a digraph
def convert_quasy_mealy_machine_to_digraph(mealy_file, prop_map, inputs, outputs, starting_player):
    try:
        o = open(mealy_file, 'r')
    except IOError:
        print "File "  + mealy_file + " not found."
        exit(0)
        
    # Create a digraph to represent this strategy
    g = digraph()
    g.__init__()
        
    l = o.readline()
    nb_states = 0
    initial_state = -1
    while l!="":
        if l.startswith("<state sid="):
            state_index = int(l.split("\"")[1]) 
            g.add_node(state_index)
            g.add_node_attribute(state_index, ("label", str(nb_states)))
            nb_states += 1
        elif l.startswith("<transition tid="):
            state_from = int(o.readline().replace("<from>", "").replace("</from>", ""))    
            state_to = int(o.readline().replace("<to>", "").replace("</to>", ""))
            gff_label = o.readline().replace("<read>", "").replace("</read>", "")
            label = convert_label_from_gff_format(gff_label, prop_map, inputs, outputs, starting_player)
            if not g.has_edge((state_from, state_to)): # new edge from state_from to state_to
                g.add_edge((state_from, state_to), 1, label)
            else: # existing edge
                new_label = g.edge_label((state_from, state_to)) + " || " + label
                g.set_edge_label((state_from, state_to), new_label)
        elif l.startswith("<initialStateSet>"):
            initial_state = int(o.readline().replace("<stateID>", "").replace("</stateID>", ""))
                
        l = o.readline()
        
    o.close()
    
    if initial_state != -1:
        g.add_node_attribute(initial_state, ('initial', True))
    else:
        print "No initial state found in Mealy machine output by Quasy"
        exit(0)
    
    return (g, initial_state)
        
#### Retrieves the expected value of the initial state of the optimal average case strategy
def get_quasy_expected_value(path, filename, initial_state_index):
    try:
        o = open(path + '/' + filename+"_Quasy/results.quasy" , 'r')
    except IOError:
        print "File " + path + '/' + filename+"_Quasy/results.quasy not found."
        exit(0)
        
    l = o.readline()
    while l != "":
        if l.startswith("State " + str(initial_state_index) + " has value"):
            o.close()
            return float(l.replace("\n", "").split(" : ")[1])
        l = o.readline()
        